From 52af7c63b9438982018d43ec02c39b102516f06d Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 16:44:19 +0100
Subject: [PATCH 01/19] Add loop guards without preconditions to invariant

---
 prusti-interface/src/prusti_error.rs          |  11 +
 prusti-viper/src/encoder/encoder.rs           |  17 ++
 prusti-viper/src/encoder/procedure_encoder.rs | 260 ++++++++++++++++--
 vir/defs/polymorphic/ast/function.rs          |   4 +-
 4 files changed, 273 insertions(+), 19 deletions(-)

diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs
index 72c4883d98e..c0515c24e13 100644
--- a/prusti-interface/src/prusti_error.rs
+++ b/prusti-interface/src/prusti_error.rs
@@ -100,6 +100,17 @@ impl PrustiError {
         )
     }
 
+    /// Issue with loop invariants (e.g. cannot automatically include loop guard)
+    pub fn loop_invariant<S: ToString>(message: S, span: MultiSpan) -> Self {
+        check_message(message.to_string());
+        let mut err = PrustiError::new(
+            format!("[Prusti: loop invariant] {}", message.to_string()),
+            span
+        );
+        err.is_error = false;
+        err
+    }
+
     /// Report an internal error of Prusti (e.g. failure of the fold-unfold)
     pub fn internal<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs
index 3ec9e008a23..514d43f6b4c 100644
--- a/prusti-viper/src/encoder/encoder.rs
+++ b/prusti-viper/src/encoder/encoder.rs
@@ -264,6 +264,23 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> {
         }
     }
 
+    pub(super) fn fun_preconds(&self, ident: &str) -> Vec<vir::Expr> {
+        let identifier = &ident.to_string().into();
+        // TODO: if we have generic args, the name stored will be `m_foo__$TY$__GAs`
+        // But the `ident` passed in will be `m_foo`
+        self.ensure_pure_function_encoded(identifier).unwrap();
+        if self.functions.borrow().contains_key(identifier) {
+            let map = self.functions.borrow();
+            map[identifier].pres.clone()
+        } else if self.contains_snapshot_function(identifier) {
+            self.get_snapshot_function(identifier).pres.clone()
+        } else if ident.starts_with("builtin") {
+            Vec::new()
+        } else {
+            unreachable!("Not found function: {:?}", identifier)
+        }
+    }
+
     pub(super) fn get_builtin_methods(
         &self
     ) -> Ref<'_, FxHashMap<BuiltinMethodKind, vir::BodylessMethod>> {
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 8600f40df2c..7d0bc585553 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -31,7 +31,7 @@ use vir_crate::{
         self as vir,
         borrows::Borrow,
         collect_assigned_vars,
-        CfgBlockIndex, Expr, ExprIterator, Successor, Type},
+        CfgBlockIndex, Expr, ExprIterator, StmtWalker, Successor, Type},
 };
 use prusti_interface::{
     data::ProcedureDefId,
@@ -43,6 +43,7 @@ use prusti_interface::{
         },
         BasicBlockIndex, PermissionKind, Procedure,
     },
+    PrustiError,
 };
 use prusti_interface::utils;
 use rustc_middle::mir::Mutability;
@@ -510,6 +511,110 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         Ok(still_unresolved_edges)
     }
 
+    fn stmt_preconditions(&self, stmt: &vir::Stmt) -> Vec<vir::Expr> {
+        struct FindFnApps<'a, 'b, 'c>(Vec<vir::Expr>, &'a Encoder<'b, 'c>);
+        impl<'a, 'b, 'c> StmtWalker for FindFnApps<'a, 'b, 'c> {
+            fn walk_exhale(&mut self, statement: &vir::Exhale) {
+                self.0.push(statement.expr.clone());
+            }
+            fn walk_assert(&mut self, statement: &vir::Assert) {
+                self.0.push(statement.expr.clone());
+            }
+            fn walk_method_call(&mut self, statement: &vir::MethodCall) {
+                self.0.extend(self.1.fun_preconds(&statement.method_name));
+                for arg in &statement.arguments {
+                    self.walk_expr(arg);
+                }
+            }
+            fn walk_expr(&mut self, expr: &vir::Expr) {
+                match expr {
+                    vir::Expr::Local(_) |
+                    vir::Expr::Const(_) |
+                    vir::Expr::MagicWand(_) => {}, // TODO: Is this correct?
+
+                    vir::Expr::Variant(vir::Variant { base, .. }) |
+                    vir::Expr::Field(vir::FieldExpr { base, .. }) |
+                    vir::Expr::AddrOf(vir::AddrOf { base, .. }) |
+                    vir::Expr::LabelledOld(vir::LabelledOld { base, .. }) |
+                    vir::Expr::FieldAccessPredicate(vir::FieldAccessPredicate { base, .. }) |
+                    vir::Expr::Unfolding(vir::Unfolding { base, .. }) |
+                    vir::Expr::SnapApp(vir::SnapApp { base, .. }) |
+                    vir::Expr::Cast(vir::Cast { base, .. }) => self.walk_expr(&*base),
+
+                    vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate { argument, .. }) |
+                    vir::Expr::UnaryOp(vir::UnaryOp { argument, .. }) =>
+                        self.walk_expr(&*argument),
+
+                    vir::Expr::BinOp(vir::BinOp { left, right, .. }) |
+                    vir::Expr::ContainerOp(vir::ContainerOp { left, right, .. }) => {
+                        self.walk_expr(&*left);
+                        self.walk_expr(&*right);
+                    }
+
+                    vir::Expr::Cond(vir::Cond { guard, then_expr, else_expr, .. }) => {
+                        self.walk_expr(&*guard);
+                        self.walk_expr(&*then_expr);
+                        self.walk_expr(&*else_expr);
+                    }
+                    vir::Expr::ForAll(vir::ForAll { body, .. }) |
+                    vir::Expr::Exists(vir::Exists { body, .. }) => self.walk_expr(&*body),
+                    vir::Expr::LetExpr(vir::LetExpr { def, body, ..}) => {
+                        self.walk_expr(&*def);
+                        self.walk_expr(&*body);
+                    }
+                    vir::Expr::FuncApp(vir::FuncApp { function_name, arguments, .. }) => {
+                        self.0.extend(self.1.fun_preconds(&function_name));
+                        for expr in arguments {
+                            self.walk_expr(expr);
+                        }
+                    },
+                    vir::Expr::DomainFuncApp(vir::DomainFuncApp { arguments, .. }) => {
+                        for expr in arguments {
+                            self.walk_expr(expr);
+                        }
+                    }
+                    vir::Expr::InhaleExhale(ie) => {
+                        self.0.push((*ie.exhale_expr).clone());
+                    }
+                    vir::Expr::Seq(vir::Seq { elements, .. }) => {
+                        for expr in elements {
+                            self.walk_expr(expr);
+                        }
+                    }
+                    vir::Expr::Downcast(vir::DowncastExpr { enum_place, base, .. }) => {
+                        self.walk_expr(&*enum_place);
+                        self.walk_expr(&*base);
+                    }
+                }
+            }
+        }
+        let mut walker = FindFnApps(Vec::new(), self.encoder);
+        walker.walk(stmt);
+        walker.0.into_iter().filter(|exp| !matches!(
+                exp,
+                vir::Expr::Const(vir::ConstExpr {
+                    value: vir::Const::Bool(true), ..
+                })
+            )
+        ).collect()
+    }
+    fn block_preconditions(&self, block: &CfgBlockIndex) -> Vec<vir::Expr> {
+        let bb = &self.cfg_method.basic_blocks[block.block_index];
+        let mut preconds: Vec<_> = bb.stmts.iter().flat_map(|stmt| self.stmt_preconditions(stmt)).collect();
+        match &bb.successor {
+            Successor::Undefined => {}
+            Successor::Return => {}
+            Successor::Goto(cbi) => preconds.extend(self.block_preconditions(cbi)),
+            Successor::GotoSwitch(succs, def) => {
+                preconds.extend(
+                    succs.iter().flat_map(|cond_bb| self.block_preconditions(&cond_bb.1))
+                );
+                preconds.extend(self.block_preconditions(def));
+            },
+        }
+        preconds
+    }
+
     /// Encodes a loop.
     ///
     /// Returns:
@@ -661,26 +766,82 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 loop_label_prefix
             ))],
         );
-        let inv_post_block = self.cfg_method.add_block(
-            &format!("{}_inv_post", loop_label_prefix),
+        let inv_post_block_perms = self.cfg_method.add_block(
+            &format!("{}_inv_post_perm", loop_label_prefix),
             vec![vir::Stmt::comment(format!(
-                "========== {}_inv_post ==========",
+                "========== {}_inv_post_perm ==========",
+                loop_label_prefix
+            ))],
+        );
+        let inv_post_block_fnspc = self.cfg_method.add_block(
+            &format!("{}_inv_post_fnspc", loop_label_prefix),
+            vec![vir::Stmt::comment(format!(
+                "========== {}_inv_post_fnspc ==========",
                 loop_label_prefix
             ))],
         );
         heads.push(Some(inv_pre_block));
         self.cfg_method
-            .set_successor(inv_pre_block, vir::Successor::Goto(inv_post_block));
+                .set_successor(inv_pre_block, vir::Successor::Goto(inv_post_block_perms));
         {
             let stmts =
                 self.encode_loop_invariant_exhale_stmts(loop_head, before_invariant_block, false)?;
             self.cfg_method.add_stmts(inv_pre_block, stmts);
         }
         // We'll add later more statements at the end of inv_pre_block, to havoc local variables
+        let fnspec_span = {
+            let (stmts, fnspec_span) =
+                self.encode_loop_invariant_inhale_fnspec_stmts(loop_head, before_invariant_block, false)?;
+            self.cfg_method.add_stmts(inv_post_block_fnspc, stmts); fnspec_span
+        };
         {
             let stmts =
-                self.encode_loop_invariant_inhale_stmts(loop_head, before_invariant_block, false)?;
-            self.cfg_method.add_stmts(inv_post_block, stmts);
+                self.encode_loop_invariant_inhale_perm_stmts(loop_head, before_invariant_block, false).with_span(fnspec_span)?;
+            self.cfg_method.add_stmts(inv_post_block_perms, stmts);
+        }
+
+        let old_len = self.cfg_method.basic_blocks.len();
+        // Encode the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end)
+        let (mid_g_head, mid_g_edges) = self.encode_blocks_group(
+            &format!("{}_group2a_", loop_label_prefix),
+            loop_guard_evaluation,
+            loop_depth,
+            return_block,
+        )?;
+        let mut preconds = mid_g_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default();
+
+        // Encode the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end)
+        let (mid_b1_head, mid_b1_edges) = self.encode_blocks_group(
+            &format!("{}_group2b_", loop_label_prefix),
+            loop_body_before_inv,
+            loop_depth,
+            return_block,
+        )?;
+        preconds.extend(mid_b1_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default());
+
+        if preconds.len() != 0 {
+            // Cannot add loop guard to loop invariant
+            let warning_msg = "the loop guard was not automatically added as a `body_invariant` \
+                (it requires the viper preconditions: [".to_string() + &preconds.iter().map(|pe|
+                    format!("{}", pe)
+                ).collect::<Vec<_>>().join(", ") + "] to hold)";
+            // Span of loop guard
+            let span_lg = loop_guard_evaluation.last().map(|bb| self.mir_encoder.get_span_of_basic_block(*bb));
+            // Span of entire loop body before inv; the last elem (if any) will be the `body_invariant!(...)` bb
+            let span_lb = loop_body_before_inv.iter().rev().skip(1).map(|bb| self.mir_encoder.get_span_of_basic_block(*bb))
+                .fold(None, |acc: Option<Span>, span| Some(acc.map(|other| 
+                    if span.ctxt() == other.ctxt() { span.to(other) } else { other }
+                ).unwrap_or(span)) );
+            // Multispan to highlight both
+            let span = MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().filter_map(|span| span).collect());
+            // It's only a warning so we might as well emit it straight away
+            PrustiError::loop_invariant(warning_msg, span).emit(self.encoder.env());
+
+            // Delete unrolled blocks
+            for i in old_len..self.cfg_method.basic_blocks.len() {
+                self.cfg_method.basic_blocks[i].stmts = vec![];
+                self.cfg_method.basic_blocks[i].successor = Successor::Return;
+            }
         }
 
         // Encode the last B2 group (start - G - B1 - invariant - *B2* - G - B1 - end)
@@ -762,10 +923,55 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
         })?);
 
+        if preconds.len() == 0 {
+            let mid_b1_block = mid_b1_head.unwrap_or(inv_post_block_fnspc);
+            // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - G - B1 - invariant_fnspec - B2 - G - B1 - end)
+            self.cfg_method
+                .set_successor(inv_post_block_perms, vir::Successor::Goto(mid_g_head.unwrap_or(mid_b1_block)));
+
+            for (curr_block, target) in &mid_g_edges {
+                if self.loop_encoder.get_loop_depth(*target) < loop_depth {
+                    self.cfg_method.set_successor(*curr_block, Successor::Return);
+                }
+            }
+            let mid_g_edges = mid_g_edges.into_iter().filter(|(_, target)|
+                self.loop_encoder.get_loop_depth(*target) >= loop_depth
+            ).collect::<Vec<_>>();
+            // Link edges from the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end)
+            still_unresolved_edges.extend(self.encode_unresolved_edges(mid_g_edges, |bb| {
+                if bb == after_guard_block {
+                    Some(mid_b1_block)
+                } else {
+                    None
+                }
+            })?);
+
+            for (curr_block, target) in &mid_b1_edges {
+                if self.loop_encoder.get_loop_depth(*target) < loop_depth {
+                    self.cfg_method.set_successor(*curr_block, Successor::Return);
+                }
+            }
+            let mid_b1_edges = mid_b1_edges.into_iter().filter(|(_, target)|
+                self.loop_encoder.get_loop_depth(*target) >= loop_depth
+            ).collect::<Vec<_>>();
+            // Link edges from the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end)
+            still_unresolved_edges.extend(self.encode_unresolved_edges(mid_b1_edges, |bb| {
+                if bb == after_inv_block {
+                    Some(inv_post_block_fnspc)
+                } else {
+                    None
+                }
+            })?);
+        } else {
+            // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - invariant_fnspec - B2 - G - B1 - end)
+            self.cfg_method
+                .set_successor(inv_post_block_perms, vir::Successor::Goto(inv_post_block_fnspc));
+        }
+
         // Link edges of "invariant" (start - G - B1 - *invariant* - B2 - G - B1 - end)
         let following_block = heads[4..].iter().find(|x| x.is_some()).unwrap().unwrap();
         self.cfg_method
-            .set_successor(inv_post_block, vir::Successor::Goto(following_block));
+            .set_successor(inv_post_block_fnspc, vir::Successor::Goto(following_block));
 
         // Link edges from the last B2 group (start - G - B1 - invariant - *B2* - G - B1 - end)
         let following_block = heads[5..].iter().find(|x| x.is_some()).unwrap().unwrap();
@@ -826,7 +1032,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         // Done. Phew!
         Ok((start_block, still_unresolved_edges))
-}
+    }
 
     /// Encode a block.
     ///
@@ -5031,28 +5237,25 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         Ok(stmts)
     }
 
-    fn encode_loop_invariant_inhale_stmts(
+    fn encode_loop_invariant_inhale_perm_stmts(
         &mut self,
         loop_head: BasicBlockIndex,
         loop_inv_block: BasicBlockIndex,
         after_loop: bool,
-    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
+    ) -> EncodingResult<Vec<vir::Stmt>> {
         trace!(
-            "[enter] encode_loop_invariant_inhale_stmts loop_head={:?} after_loop={}",
+            "[enter] encode_loop_invariant_inhale_perm_stmts loop_head={:?} after_loop={}",
             loop_head,
             after_loop
         );
-        let (func_spec, func_spec_span) =
-            self.encode_loop_invariant_specs(loop_head, loop_inv_block)?;
         let (permissions, equalities, invs_spec) =
-            self.encode_loop_invariant_permissions(loop_head, loop_inv_block, true)
-                .with_span(func_spec_span)?;
+            self.encode_loop_invariant_permissions(loop_head, loop_inv_block, true)?;
 
         let permission_expr = permissions.into_iter().conjoin();
         let equality_expr = equalities.into_iter().conjoin();
 
         let mut stmts = vec![vir::Stmt::comment(format!(
-            "Inhale the loop invariant of block {:?}",
+            "Inhale the loop permissions invariant of block {:?}",
             loop_head
         ))];
         stmts.push(vir::Stmt::Inhale( vir::Inhale {
@@ -5064,10 +5267,31 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         stmts.push(vir::Stmt::Inhale( vir::Inhale {
             expr: invs_spec.into_iter().conjoin(),
         }));
+        Ok(stmts)
+    }
+
+    fn encode_loop_invariant_inhale_fnspec_stmts(
+        &mut self,
+        loop_head: BasicBlockIndex,
+        loop_inv_block: BasicBlockIndex,
+        after_loop: bool,
+    ) -> SpannedEncodingResult<(Vec<vir::Stmt>, MultiSpan)> {
+        trace!(
+            "[enter] encode_loop_invariant_inhale_fnspec_stmts loop_head={:?} after_loop={}",
+            loop_head,
+            after_loop
+        );
+        let (func_spec, func_spec_span) =
+            self.encode_loop_invariant_specs(loop_head, loop_inv_block)?;
+
+        let mut stmts = vec![vir::Stmt::comment(format!(
+            "Inhale the loop fnspec invariant of block {:?}",
+            loop_head
+        ))];
         stmts.push(vir::Stmt::Inhale( vir::Inhale {
             expr: func_spec.into_iter().conjoin(),
         }));
-        Ok(stmts)
+        Ok((stmts, func_spec_span))
     }
 
     fn encode_prusti_local(&self, local: Local) -> vir::LocalVar {
diff --git a/vir/defs/polymorphic/ast/function.rs b/vir/defs/polymorphic/ast/function.rs
index 9a74b6c3f72..b5e57b19bcc 100644
--- a/vir/defs/polymorphic/ast/function.rs
+++ b/vir/defs/polymorphic/ast/function.rs
@@ -105,7 +105,9 @@ pub fn compute_identifier(
 ) -> String {
     let mut identifier = name.to_string();
     // Include the signature of the function in the function name
-    identifier.push_str("__$TY$__");
+    if type_arguments.len() > 0 {
+        identifier.push_str("__$TY$__");
+    }
     fn type_name(typ: &Type) -> String {
         match typ {
             Type::Int => "$int$".to_string(),

From 1b9ed1aee75e79bd2438b8d1cbf0f290e664dd42 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 17:06:10 +0100
Subject: [PATCH 02/19] Avoid unnecessary encoding

We can check the encoded Viper of the first encoding of `G` and `B1`, before the loop
---
 prusti-viper/src/encoder/procedure_encoder.rs | 57 ++++++++++---------
 1 file changed, 30 insertions(+), 27 deletions(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 7d0bc585553..12d605ec17c 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -756,6 +756,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         )?;
         heads.push(first_b1_head);
 
+        // Calculate if `G` and `B1` are safe to include as the first `body_invariant!(...)`
+        let mut preconds = first_g_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default();
+        preconds.extend(first_b1_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default());
+
         // Build the "invariant" CFG block (start - G - B1 - *invariant* - B2 - G - B1 - end)
         // (1) checks the loop invariant on entry
         // (2) havocs the invariant and the local variables.
@@ -800,26 +804,25 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             self.cfg_method.add_stmts(inv_post_block_perms, stmts);
         }
 
-        let old_len = self.cfg_method.basic_blocks.len();
-        // Encode the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end)
-        let (mid_g_head, mid_g_edges) = self.encode_blocks_group(
-            &format!("{}_group2a_", loop_label_prefix),
-            loop_guard_evaluation,
-            loop_depth,
-            return_block,
-        )?;
-        let mut preconds = mid_g_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default();
-
-        // Encode the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end)
-        let (mid_b1_head, mid_b1_edges) = self.encode_blocks_group(
-            &format!("{}_group2b_", loop_label_prefix),
-            loop_body_before_inv,
-            loop_depth,
-            return_block,
-        )?;
-        preconds.extend(mid_b1_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default());
+        let mid_groups = if preconds.len() == 0 {
+            // Encode the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end)
+            let mid_g = self.encode_blocks_group(
+                &format!("{}_group2a_", loop_label_prefix),
+                loop_guard_evaluation,
+                loop_depth,
+                return_block,
+            )?;
 
-        if preconds.len() != 0 {
+            // Encode the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end)
+            let mid_b1 = self.encode_blocks_group(
+                &format!("{}_group2b_", loop_label_prefix),
+                loop_body_before_inv,
+                loop_depth,
+                return_block,
+            )?;
+            // Save for later linking up
+            Some((mid_g, mid_b1))
+        } else {
             // Cannot add loop guard to loop invariant
             let warning_msg = "the loop guard was not automatically added as a `body_invariant` \
                 (it requires the viper preconditions: [".to_string() + &preconds.iter().map(|pe|
@@ -836,13 +839,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let span = MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().filter_map(|span| span).collect());
             // It's only a warning so we might as well emit it straight away
             PrustiError::loop_invariant(warning_msg, span).emit(self.encoder.env());
-
-            // Delete unrolled blocks
-            for i in old_len..self.cfg_method.basic_blocks.len() {
-                self.cfg_method.basic_blocks[i].stmts = vec![];
-                self.cfg_method.basic_blocks[i].successor = Successor::Return;
-            }
-        }
+            None
+        };
 
         // Encode the last B2 group (start - G - B1 - invariant - *B2* - G - B1 - end)
         let (last_b2_head, last_b2_edges) = self.encode_blocks_group(
@@ -923,12 +921,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
         })?);
 
-        if preconds.len() == 0 {
+        if let Some(((mid_g_head, mid_g_edges), (mid_b1_head, mid_b1_edges))) = mid_groups {
             let mid_b1_block = mid_b1_head.unwrap_or(inv_post_block_fnspc);
             // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - G - B1 - invariant_fnspec - B2 - G - B1 - end)
             self.cfg_method
                 .set_successor(inv_post_block_perms, vir::Successor::Goto(mid_g_head.unwrap_or(mid_b1_block)));
 
+            // We know that there is at least one loop iteration of B2, thus it is safe to assume
+            // that anything beforehand couldn't have exited the loop. Here we use
+            // `self.cfg_method.set_successor(..., Successor::Return)` as the same as `assume false`
             for (curr_block, target) in &mid_g_edges {
                 if self.loop_encoder.get_loop_depth(*target) < loop_depth {
                     self.cfg_method.set_successor(*curr_block, Successor::Return);
@@ -946,6 +947,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 }
             })?);
 
+            // We know that there is at least one loop iteration of B2, thus it is safe to assume
+            // that anything beforehand couldn't have exited the loop.
             for (curr_block, target) in &mid_b1_edges {
                 if self.loop_encoder.get_loop_depth(*target) < loop_depth {
                     self.cfg_method.set_successor(*curr_block, Successor::Return);

From fc978a937b4dcdc04f3c584702f6cb926b25d9f3 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 17:32:07 +0100
Subject: [PATCH 03/19] Clippy fix and ignore AccessPredicate expressions

---
 prusti-viper/src/encoder/procedure_encoder.rs | 3 +++
 vir/defs/polymorphic/ast/function.rs          | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 12d605ec17c..8d3fbebf98a 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -592,9 +592,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         walker.walk(stmt);
         walker.0.into_iter().filter(|exp| !matches!(
                 exp,
+                // Note: This doesn't remove e.g. `true && acc(Pred(...), ...)`
                 vir::Expr::Const(vir::ConstExpr {
                     value: vir::Const::Bool(true), ..
                 })
+                | vir::Expr::PredicateAccessPredicate(_)
+                | vir::Expr::FieldAccessPredicate(_)
             )
         ).collect()
     }
diff --git a/vir/defs/polymorphic/ast/function.rs b/vir/defs/polymorphic/ast/function.rs
index b5e57b19bcc..f2e9a2c376a 100644
--- a/vir/defs/polymorphic/ast/function.rs
+++ b/vir/defs/polymorphic/ast/function.rs
@@ -105,7 +105,7 @@ pub fn compute_identifier(
 ) -> String {
     let mut identifier = name.to_string();
     // Include the signature of the function in the function name
-    if type_arguments.len() > 0 {
+    if !type_arguments.is_empty() {
         identifier.push_str("__$TY$__");
     }
     fn type_name(typ: &Type) -> String {

From 9fc7dc071846ac4f11c6872620cd9c48078d6bee Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 17:54:06 +0100
Subject: [PATCH 04/19] Fix issue with resolving function calls

---
 prusti-viper/src/encoder/encoder.rs           | 17 -----------------
 prusti-viper/src/encoder/procedure_encoder.rs | 11 ++++++++---
 2 files changed, 8 insertions(+), 20 deletions(-)

diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs
index 514d43f6b4c..3ec9e008a23 100644
--- a/prusti-viper/src/encoder/encoder.rs
+++ b/prusti-viper/src/encoder/encoder.rs
@@ -264,23 +264,6 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> {
         }
     }
 
-    pub(super) fn fun_preconds(&self, ident: &str) -> Vec<vir::Expr> {
-        let identifier = &ident.to_string().into();
-        // TODO: if we have generic args, the name stored will be `m_foo__$TY$__GAs`
-        // But the `ident` passed in will be `m_foo`
-        self.ensure_pure_function_encoded(identifier).unwrap();
-        if self.functions.borrow().contains_key(identifier) {
-            let map = self.functions.borrow();
-            map[identifier].pres.clone()
-        } else if self.contains_snapshot_function(identifier) {
-            self.get_snapshot_function(identifier).pres.clone()
-        } else if ident.starts_with("builtin") {
-            Vec::new()
-        } else {
-            unreachable!("Not found function: {:?}", identifier)
-        }
-    }
-
     pub(super) fn get_builtin_methods(
         &self
     ) -> Ref<'_, FxHashMap<BuiltinMethodKind, vir::BodylessMethod>> {
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 8d3fbebf98a..039c06342be 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -29,6 +29,7 @@ use prusti_common::{
 use vir_crate::{
     polymorphic::{
         self as vir,
+        compute_identifier,
         borrows::Borrow,
         collect_assigned_vars,
         CfgBlockIndex, Expr, ExprIterator, StmtWalker, Successor, Type},
@@ -521,7 +522,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 self.0.push(statement.expr.clone());
             }
             fn walk_method_call(&mut self, statement: &vir::MethodCall) {
-                self.0.extend(self.1.fun_preconds(&statement.method_name));
+                if !statement.method_name.starts_with("builtin$havoc") {
+                    todo!("Unclear how to handle call to {}", statement.method_name);
+                }
                 for arg in &statement.arguments {
                     self.walk_expr(arg);
                 }
@@ -562,8 +565,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                         self.walk_expr(&*def);
                         self.walk_expr(&*body);
                     }
-                    vir::Expr::FuncApp(vir::FuncApp { function_name, arguments, .. }) => {
-                        self.0.extend(self.1.fun_preconds(&function_name));
+                    vir::Expr::FuncApp(vir::FuncApp { function_name, type_arguments, arguments, formal_arguments, return_type, .. }) => {
+                        let identifier: vir::FunctionIdentifier =
+                            compute_identifier(function_name, type_arguments, formal_arguments, return_type).into();
+                        self.0.extend(self.1.get_function(&identifier).unwrap().pres.clone());
                         for expr in arguments {
                             self.walk_expr(expr);
                         }

From d4fe137122f7facfe22f319cc13942fe5423fe5a Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 17:55:42 +0100
Subject: [PATCH 05/19] Clippy fixes

---
 prusti-viper/src/encoder/procedure_encoder.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 039c06342be..3910f9ca8f9 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -812,7 +812,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             self.cfg_method.add_stmts(inv_post_block_perms, stmts);
         }
 
-        let mid_groups = if preconds.len() == 0 {
+        let mid_groups = if preconds.is_empty() {
             // Encode the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end)
             let mid_g = self.encode_blocks_group(
                 &format!("{}_group2a_", loop_label_prefix),
@@ -844,7 +844,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     if span.ctxt() == other.ctxt() { span.to(other) } else { other }
                 ).unwrap_or(span)) );
             // Multispan to highlight both
-            let span = MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().filter_map(|span| span).collect());
+            let span = MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().flatten().collect());
             // It's only a warning so we might as well emit it straight away
             PrustiError::loop_invariant(warning_msg, span).emit(self.encoder.env());
             None

From d33480843e8eef681ca6eb9e39a30b0b92cf01f4 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 18:00:25 +0100
Subject: [PATCH 06/19] Remove unnecessary check of MethodCall

Trusting what https://github.com/viperproject/prusti-dev/blob/d53bdd7af1dda31d763e5fce83b2829aa1164a79/prusti-viper/src/encoder/foldunfold/semantics.rs#L75 says
---
 prusti-viper/src/encoder/procedure_encoder.rs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 3910f9ca8f9..61e042275a9 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -522,9 +522,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 self.0.push(statement.expr.clone());
             }
             fn walk_method_call(&mut self, statement: &vir::MethodCall) {
-                if !statement.method_name.starts_with("builtin$havoc") {
-                    todo!("Unclear how to handle call to {}", statement.method_name);
-                }
+                // Note: We know that in Prusti method's preconditions and postconditions are empty
                 for arg in &statement.arguments {
                     self.walk_expr(arg);
                 }

From af55365036ebdc4c4788b1dff0d6f0fc47f4c8c5 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 20:35:01 +0100
Subject: [PATCH 07/19] Make use of ExprFolder

---
 prusti-viper/src/encoder/procedure_encoder.rs | 148 ++++++++----------
 1 file changed, 68 insertions(+), 80 deletions(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 61e042275a9..475deb31846 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -32,7 +32,7 @@ use vir_crate::{
         compute_identifier,
         borrows::Borrow,
         collect_assigned_vars,
-        CfgBlockIndex, Expr, ExprIterator, StmtWalker, Successor, Type},
+        CfgBlockIndex, Expr, ExprIterator, Successor, Type},
 };
 use prusti_interface::{
     data::ProcedureDefId,
@@ -513,96 +513,84 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     }
 
     fn stmt_preconditions(&self, stmt: &vir::Stmt) -> Vec<vir::Expr> {
-        struct FindFnApps<'a, 'b, 'c>(Vec<vir::Expr>, &'a Encoder<'b, 'c>);
+        use vir::{ExprFolder, StmtWalker};
+        struct FindFnApps<'a, 'b, 'c> {
+            recurse: bool,
+            preconds: Vec<vir::Expr>,
+            encoder: &'a Encoder<'b, 'c>,
+        }
+        fn is_const_true(expr: &vir::Expr) -> bool {
+            matches!(
+                expr,
+                vir::Expr::Const(vir::ConstExpr {
+                    value: vir::Const::Bool(true), ..
+                })
+            )
+        }
         impl<'a, 'b, 'c> StmtWalker for FindFnApps<'a, 'b, 'c> {
             fn walk_exhale(&mut self, statement: &vir::Exhale) {
-                self.0.push(statement.expr.clone());
+                let expr = self.fold(statement.expr.clone());
+                self.preconds.push(expr);
             }
             fn walk_assert(&mut self, statement: &vir::Assert) {
-                self.0.push(statement.expr.clone());
-            }
-            fn walk_method_call(&mut self, statement: &vir::MethodCall) {
-                // Note: We know that in Prusti method's preconditions and postconditions are empty
-                for arg in &statement.arguments {
-                    self.walk_expr(arg);
-                }
+                let expr = self.fold(statement.expr.clone());
+                self.preconds.push(expr);
             }
             fn walk_expr(&mut self, expr: &vir::Expr) {
-                match expr {
-                    vir::Expr::Local(_) |
-                    vir::Expr::Const(_) |
-                    vir::Expr::MagicWand(_) => {}, // TODO: Is this correct?
-
-                    vir::Expr::Variant(vir::Variant { base, .. }) |
-                    vir::Expr::Field(vir::FieldExpr { base, .. }) |
-                    vir::Expr::AddrOf(vir::AddrOf { base, .. }) |
-                    vir::Expr::LabelledOld(vir::LabelledOld { base, .. }) |
-                    vir::Expr::FieldAccessPredicate(vir::FieldAccessPredicate { base, .. }) |
-                    vir::Expr::Unfolding(vir::Unfolding { base, .. }) |
-                    vir::Expr::SnapApp(vir::SnapApp { base, .. }) |
-                    vir::Expr::Cast(vir::Cast { base, .. }) => self.walk_expr(&*base),
-
-                    vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate { argument, .. }) |
-                    vir::Expr::UnaryOp(vir::UnaryOp { argument, .. }) =>
-                        self.walk_expr(&*argument),
-
-                    vir::Expr::BinOp(vir::BinOp { left, right, .. }) |
-                    vir::Expr::ContainerOp(vir::ContainerOp { left, right, .. }) => {
-                        self.walk_expr(&*left);
-                        self.walk_expr(&*right);
-                    }
-
-                    vir::Expr::Cond(vir::Cond { guard, then_expr, else_expr, .. }) => {
-                        self.walk_expr(&*guard);
-                        self.walk_expr(&*then_expr);
-                        self.walk_expr(&*else_expr);
-                    }
-                    vir::Expr::ForAll(vir::ForAll { body, .. }) |
-                    vir::Expr::Exists(vir::Exists { body, .. }) => self.walk_expr(&*body),
-                    vir::Expr::LetExpr(vir::LetExpr { def, body, ..}) => {
-                        self.walk_expr(&*def);
-                        self.walk_expr(&*body);
-                    }
-                    vir::Expr::FuncApp(vir::FuncApp { function_name, type_arguments, arguments, formal_arguments, return_type, .. }) => {
-                        let identifier: vir::FunctionIdentifier =
-                            compute_identifier(function_name, type_arguments, formal_arguments, return_type).into();
-                        self.0.extend(self.1.get_function(&identifier).unwrap().pres.clone());
-                        for expr in arguments {
-                            self.walk_expr(expr);
-                        }
-                    },
-                    vir::Expr::DomainFuncApp(vir::DomainFuncApp { arguments, .. }) => {
-                        for expr in arguments {
-                            self.walk_expr(expr);
-                        }
-                    }
-                    vir::Expr::InhaleExhale(ie) => {
-                        self.0.push((*ie.exhale_expr).clone());
-                    }
-                    vir::Expr::Seq(vir::Seq { elements, .. }) => {
-                        for expr in elements {
-                            self.walk_expr(expr);
-                        }
-                    }
-                    vir::Expr::Downcast(vir::DowncastExpr { enum_place, base, .. }) => {
-                        self.walk_expr(&*enum_place);
-                        self.walk_expr(&*base);
+                self.fold(expr.clone());
+            }
+        }
+        impl<'a, 'b, 'c> ExprFolder for FindFnApps<'a, 'b, 'c> { 
+            fn fold_func_app(&mut self, expr: vir::FuncApp) -> vir::Expr {
+                let vir::FuncApp { function_name, type_arguments, arguments, formal_arguments, return_type, .. } = expr;
+                if self.recurse {
+                    let identifier: vir::FunctionIdentifier =
+                                compute_identifier(&function_name, &type_arguments, &formal_arguments, &return_type).into();
+                    let pres = self.encoder.get_function(&identifier).unwrap().pres.clone();
+                    // Avoid recursively collecting preconditions: they should be self-framing anyway
+                    self.recurse = false;
+                    let pres = pres.into_iter().map(|expr| self.fold(expr)).collect::<Vec<_>>();
+                    self.recurse = true;
+                    self.preconds.extend(pres);
+
+                    for arg in arguments {
+                        self.fold(arg);
                     }
                 }
+                true.into()
+            }
+            fn fold_inhale_exhale(&mut self, expr: vir::InhaleExhale) -> vir::Expr {
+                // We only care about the exhale part (e.g. for `walk_exhale`)
+                self.fold(*expr.exhale_expr)
+            }
+            fn fold_predicate_access_predicate(&mut self, expr: vir::PredicateAccessPredicate) -> vir::Expr {
+                self.fold(*expr.argument);
+                true.into()
+            }
+            fn fold_field_access_predicate(&mut self, expr: vir::FieldAccessPredicate) -> vir::Expr {
+                self.fold(*expr.base);
+                true.into()
+            }
+            fn fold_bin_op(&mut self, expr: vir::BinOp) -> vir::Expr {
+                let vir::BinOp { op_kind, left, right, position } = expr;
+                let left = self.fold_boxed(left);
+                let right = self.fold_boxed(right);
+                match op_kind {
+                    vir::BinaryOpKind::And if is_const_true(&*left) => *right,
+                    vir::BinaryOpKind::And if is_const_true(&*right) => *left,
+                    vir::BinaryOpKind::Or if is_const_true(&*left) => *left,
+                    vir::BinaryOpKind::Or if is_const_true(&*right) => *right,
+                    _ => vir::Expr::BinOp(vir::BinOp {
+                        op_kind, left, right, position,
+                    }),
+                }
             }
         }
-        let mut walker = FindFnApps(Vec::new(), self.encoder);
+        let mut walker = FindFnApps {
+            recurse: true, preconds: Vec::new(), encoder: self.encoder
+        };
         walker.walk(stmt);
-        walker.0.into_iter().filter(|exp| !matches!(
-                exp,
-                // Note: This doesn't remove e.g. `true && acc(Pred(...), ...)`
-                vir::Expr::Const(vir::ConstExpr {
-                    value: vir::Const::Bool(true), ..
-                })
-                | vir::Expr::PredicateAccessPredicate(_)
-                | vir::Expr::FieldAccessPredicate(_)
-            )
-        ).collect()
+        walker.preconds.into_iter().filter(|exp| !is_const_true(exp)).collect()
     }
     fn block_preconditions(&self, block: &CfgBlockIndex) -> Vec<vir::Expr> {
         let bb = &self.cfg_method.basic_blocks[block.block_index];

From 50a77fdaffe7bb9ce37def3a3e3569ef5a72540b Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 20:38:02 +0100
Subject: [PATCH 08/19] Fix typo

---
 vir/defs/polymorphic/ast/expr_transformers.rs | 184 +++++++++---------
 1 file changed, 92 insertions(+), 92 deletions(-)

diff --git a/vir/defs/polymorphic/ast/expr_transformers.rs b/vir/defs/polymorphic/ast/expr_transformers.rs
index ac4a8c2d2e9..107eabda8b1 100644
--- a/vir/defs/polymorphic/ast/expr_transformers.rs
+++ b/vir/defs/polymorphic/ast/expr_transformers.rs
@@ -469,85 +469,85 @@ pub trait ExprWalker: Sized {
         self.walk_type(&var.typ);
     }
 
-    fn walk_local(&mut self, statement: &Local) {
-        let Local { variable, .. } = statement;
+    fn walk_local(&mut self, expr: &Local) {
+        let Local { variable, .. } = expr;
         self.walk_local_var(variable);
     }
-    fn walk_variant(&mut self, statement: &Variant) {
+    fn walk_variant(&mut self, expr: &Variant) {
         let Variant {
             base,
             variant_index,
             ..
-        } = statement;
+        } = expr;
         self.walk(base);
         self.walk_type(&variant_index.typ);
     }
-    fn walk_field(&mut self, statement: &FieldExpr) {
-        let FieldExpr { base, field, .. } = statement;
+    fn walk_field(&mut self, expr: &FieldExpr) {
+        let FieldExpr { base, field, .. } = expr;
         self.walk(base);
         self.walk_type(&field.typ);
     }
-    fn walk_addr_of(&mut self, statement: &AddrOf) {
+    fn walk_addr_of(&mut self, expr: &AddrOf) {
         let AddrOf {
             base, addr_type, ..
-        } = statement;
+        } = expr;
         self.walk(base);
         self.walk_type(addr_type);
     }
     fn walk_const(&mut self, _const_expr: &ConstExpr) {}
-    fn walk_labelled_old(&mut self, statement: &LabelledOld) {
-        let LabelledOld { base, .. } = statement;
+    fn walk_labelled_old(&mut self, expr: &LabelledOld) {
+        let LabelledOld { base, .. } = expr;
         self.walk(base);
     }
-    fn walk_magic_wand(&mut self, statement: &MagicWand) {
-        let MagicWand { left, right, .. } = statement;
+    fn walk_magic_wand(&mut self, expr: &MagicWand) {
+        let MagicWand { left, right, .. } = expr;
         self.walk(left);
         self.walk(right);
     }
-    fn walk_predicate_access_predicate(&mut self, statement: &PredicateAccessPredicate) {
-        let PredicateAccessPredicate { argument, .. } = statement;
+    fn walk_predicate_access_predicate(&mut self, expr: &PredicateAccessPredicate) {
+        let PredicateAccessPredicate { argument, .. } = expr;
         self.walk(argument);
     }
-    fn walk_field_access_predicate(&mut self, statement: &FieldAccessPredicate) {
-        let FieldAccessPredicate { base, .. } = statement;
+    fn walk_field_access_predicate(&mut self, expr: &FieldAccessPredicate) {
+        let FieldAccessPredicate { base, .. } = expr;
         self.walk(base);
     }
-    fn walk_unary_op(&mut self, statement: &UnaryOp) {
-        let UnaryOp { argument, .. } = statement;
+    fn walk_unary_op(&mut self, expr: &UnaryOp) {
+        let UnaryOp { argument, .. } = expr;
         self.walk(argument)
     }
-    fn walk_bin_op(&mut self, statement: &BinOp) {
-        let BinOp { left, right, .. } = statement;
+    fn walk_bin_op(&mut self, expr: &BinOp) {
+        let BinOp { left, right, .. } = expr;
         self.walk(left);
         self.walk(right);
     }
-    fn walk_unfolding(&mut self, statement: &Unfolding) {
+    fn walk_unfolding(&mut self, expr: &Unfolding) {
         let Unfolding {
             arguments, base, ..
-        } = statement;
+        } = expr;
         for arg in arguments {
             self.walk(arg);
         }
         self.walk(base);
     }
-    fn walk_cond(&mut self, statement: &Cond) {
+    fn walk_cond(&mut self, expr: &Cond) {
         let Cond {
             guard,
             then_expr,
             else_expr,
             ..
-        } = statement;
+        } = expr;
         self.walk(guard);
         self.walk(then_expr);
         self.walk(else_expr);
     }
-    fn walk_forall(&mut self, statement: &ForAll) {
+    fn walk_forall(&mut self, expr: &ForAll) {
         let ForAll {
             variables,
             triggers,
             body,
             ..
-        } = statement;
+        } = expr;
         for set in triggers {
             for expr in set.elements() {
                 self.walk(expr);
@@ -558,13 +558,13 @@ pub trait ExprWalker: Sized {
         }
         self.walk(body);
     }
-    fn walk_exists(&mut self, statement: &Exists) {
+    fn walk_exists(&mut self, expr: &Exists) {
         let Exists {
             variables,
             triggers,
             body,
             ..
-        } = statement;
+        } = expr;
         for set in triggers {
             for expr in set.elements() {
                 self.walk(expr);
@@ -575,24 +575,24 @@ pub trait ExprWalker: Sized {
         }
         self.walk(body);
     }
-    fn walk_let_expr(&mut self, statement: &LetExpr) {
+    fn walk_let_expr(&mut self, expr: &LetExpr) {
         let LetExpr {
             variable,
             def,
             body,
             ..
-        } = statement;
+        } = expr;
         self.walk_local_var(variable);
         self.walk(def);
         self.walk(body);
     }
-    fn walk_func_app(&mut self, statement: &FuncApp) {
+    fn walk_func_app(&mut self, expr: &FuncApp) {
         let FuncApp {
             arguments,
             formal_arguments,
             return_type,
             ..
-        } = statement;
+        } = expr;
         for arg in arguments {
             self.walk(arg)
         }
@@ -601,12 +601,12 @@ pub trait ExprWalker: Sized {
         }
         self.walk_type(return_type);
     }
-    fn walk_domain_func_app(&mut self, statement: &DomainFuncApp) {
+    fn walk_domain_func_app(&mut self, expr: &DomainFuncApp) {
         let DomainFuncApp {
             domain_function,
             arguments,
             ..
-        } = statement;
+        } = expr;
         for arg in arguments {
             self.walk(arg)
         }
@@ -632,44 +632,44 @@ pub trait ExprWalker: Sized {
         }
     }
     */
-    fn walk_inhale_exhale(&mut self, statement: &InhaleExhale) {
+    fn walk_inhale_exhale(&mut self, expr: &InhaleExhale) {
         let InhaleExhale {
             inhale_expr,
             exhale_expr,
             ..
-        } = statement;
+        } = expr;
         self.walk(inhale_expr);
         self.walk(exhale_expr);
     }
 
-    fn walk_downcast(&mut self, statement: &DowncastExpr) {
+    fn walk_downcast(&mut self, expr: &DowncastExpr) {
         let DowncastExpr {
             base, enum_place, ..
-        } = statement;
+        } = expr;
         self.walk(base);
         self.walk(enum_place);
     }
-    fn walk_snap_app(&mut self, statement: &SnapApp) {
-        let SnapApp { base, .. } = statement;
+    fn walk_snap_app(&mut self, expr: &SnapApp) {
+        let SnapApp { base, .. } = expr;
         self.walk(base);
     }
 
-    fn walk_container_op(&mut self, statement: &ContainerOp) {
-        let ContainerOp { left, right, .. } = statement;
+    fn walk_container_op(&mut self, expr: &ContainerOp) {
+        let ContainerOp { left, right, .. } = expr;
         self.walk(left);
         self.walk(right);
     }
 
-    fn walk_seq(&mut self, statement: &Seq) {
-        let Seq { typ, elements, .. } = statement;
+    fn walk_seq(&mut self, expr: &Seq) {
+        let Seq { typ, elements, .. } = expr;
         for elem in elements {
             self.walk(elem);
         }
         self.walk_type(typ);
     }
 
-    fn walk_cast(&mut self, statement: &Cast) {
-        let Cast { base, .. } = statement;
+    fn walk_cast(&mut self, expr: &Cast) {
+        let Cast { base, .. } = expr;
         self.walk(base);
     }
 }
@@ -1149,96 +1149,96 @@ pub trait FallibleExprWalker: Sized {
         self.fallible_walk_type(&var.typ)
     }
 
-    fn fallible_walk_local(&mut self, statement: &Local) -> Result<(), Self::Error> {
-        let Local { variable, .. } = statement;
+    fn fallible_walk_local(&mut self, expr: &Local) -> Result<(), Self::Error> {
+        let Local { variable, .. } = expr;
         self.fallible_walk_local_var(variable)
     }
-    fn fallible_walk_variant(&mut self, statement: &Variant) -> Result<(), Self::Error> {
+    fn fallible_walk_variant(&mut self, expr: &Variant) -> Result<(), Self::Error> {
         let Variant {
             base,
             variant_index,
             ..
-        } = statement;
+        } = expr;
         self.fallible_walk(base)?;
         self.fallible_walk_type(&variant_index.typ)
     }
-    fn fallible_walk_field(&mut self, statement: &FieldExpr) -> Result<(), Self::Error> {
-        let FieldExpr { base, field, .. } = statement;
+    fn fallible_walk_field(&mut self, expr: &FieldExpr) -> Result<(), Self::Error> {
+        let FieldExpr { base, field, .. } = expr;
         self.fallible_walk(base)?;
         self.fallible_walk_type(&field.typ)
     }
-    fn fallible_walk_addr_of(&mut self, statement: &AddrOf) -> Result<(), Self::Error> {
+    fn fallible_walk_addr_of(&mut self, expr: &AddrOf) -> Result<(), Self::Error> {
         let AddrOf {
             base, addr_type, ..
-        } = statement;
+        } = expr;
         self.fallible_walk(base)?;
         self.fallible_walk_type(addr_type)
     }
     fn fallible_walk_const(&mut self, _const_expr: &ConstExpr) -> Result<(), Self::Error> {
         Ok(())
     }
-    fn fallible_walk_labelled_old(&mut self, statement: &LabelledOld) -> Result<(), Self::Error> {
-        let LabelledOld { base, .. } = statement;
+    fn fallible_walk_labelled_old(&mut self, expr: &LabelledOld) -> Result<(), Self::Error> {
+        let LabelledOld { base, .. } = expr;
         self.fallible_walk(base)
     }
-    fn fallible_walk_magic_wand(&mut self, statement: &MagicWand) -> Result<(), Self::Error> {
-        let MagicWand { left, right, .. } = statement;
+    fn fallible_walk_magic_wand(&mut self, expr: &MagicWand) -> Result<(), Self::Error> {
+        let MagicWand { left, right, .. } = expr;
         self.fallible_walk(left)?;
         self.fallible_walk(right)?;
         Ok(())
     }
     fn fallible_walk_predicate_access_predicate(
         &mut self,
-        statement: &PredicateAccessPredicate,
+        expr: &PredicateAccessPredicate,
     ) -> Result<(), Self::Error> {
-        let PredicateAccessPredicate { argument, .. } = statement;
+        let PredicateAccessPredicate { argument, .. } = expr;
         self.fallible_walk(argument)
     }
     fn fallible_walk_field_access_predicate(
         &mut self,
-        statement: &FieldAccessPredicate,
+        expr: &FieldAccessPredicate,
     ) -> Result<(), Self::Error> {
-        let FieldAccessPredicate { base, .. } = statement;
+        let FieldAccessPredicate { base, .. } = expr;
         self.fallible_walk(base)
     }
-    fn fallible_walk_unary_op(&mut self, statement: &UnaryOp) -> Result<(), Self::Error> {
-        let UnaryOp { argument, .. } = statement;
+    fn fallible_walk_unary_op(&mut self, expr: &UnaryOp) -> Result<(), Self::Error> {
+        let UnaryOp { argument, .. } = expr;
         self.fallible_walk(argument)
     }
-    fn fallible_walk_bin_op(&mut self, statement: &BinOp) -> Result<(), Self::Error> {
-        let BinOp { left, right, .. } = statement;
+    fn fallible_walk_bin_op(&mut self, expr: &BinOp) -> Result<(), Self::Error> {
+        let BinOp { left, right, .. } = expr;
         self.fallible_walk(left)?;
         self.fallible_walk(right)?;
         Ok(())
     }
-    fn fallible_walk_unfolding(&mut self, statement: &Unfolding) -> Result<(), Self::Error> {
+    fn fallible_walk_unfolding(&mut self, expr: &Unfolding) -> Result<(), Self::Error> {
         let Unfolding {
             arguments, base, ..
-        } = statement;
+        } = expr;
         for arg in arguments {
             self.fallible_walk(arg)?;
         }
         self.fallible_walk(base)
     }
-    fn fallible_walk_cond(&mut self, statement: &Cond) -> Result<(), Self::Error> {
+    fn fallible_walk_cond(&mut self, expr: &Cond) -> Result<(), Self::Error> {
         let Cond {
             guard,
             then_expr,
             else_expr,
             ..
-        } = statement;
+        } = expr;
         self.fallible_walk(guard)?;
         self.fallible_walk(then_expr)?;
         self.fallible_walk(else_expr)?;
         Ok(())
     }
-    fn fallible_walk_forall(&mut self, statement: &ForAll) -> Result<(), Self::Error> {
+    fn fallible_walk_forall(&mut self, expr: &ForAll) -> Result<(), Self::Error> {
         let ForAll {
             variables,
             triggers,
             body,
             ..
-        } = statement;
+        } = expr;
         for var in variables {
             self.fallible_walk_local_var(var)?;
         }
@@ -1249,13 +1249,13 @@ pub trait FallibleExprWalker: Sized {
         }
         self.fallible_walk(body)
     }
-    fn fallible_walk_exists(&mut self, statement: &Exists) -> Result<(), Self::Error> {
+    fn fallible_walk_exists(&mut self, expr: &Exists) -> Result<(), Self::Error> {
         let Exists {
             variables,
             triggers,
             body,
             ..
-        } = statement;
+        } = expr;
         for var in variables {
             self.fallible_walk_local_var(var)?;
         }
@@ -1266,25 +1266,25 @@ pub trait FallibleExprWalker: Sized {
         }
         self.fallible_walk(body)
     }
-    fn fallible_walk_let_expr(&mut self, statement: &LetExpr) -> Result<(), Self::Error> {
+    fn fallible_walk_let_expr(&mut self, expr: &LetExpr) -> Result<(), Self::Error> {
         let LetExpr {
             variable,
             def,
             body,
             ..
-        } = statement;
+        } = expr;
         self.fallible_walk_local_var(variable)?;
         self.fallible_walk(def)?;
         self.fallible_walk(body)?;
         Ok(())
     }
-    fn fallible_walk_func_app(&mut self, statement: &FuncApp) -> Result<(), Self::Error> {
+    fn fallible_walk_func_app(&mut self, expr: &FuncApp) -> Result<(), Self::Error> {
         let FuncApp {
             arguments,
             formal_arguments,
             return_type,
             ..
-        } = statement;
+        } = expr;
         for arg in arguments {
             self.fallible_walk(arg)?;
         }
@@ -1295,13 +1295,13 @@ pub trait FallibleExprWalker: Sized {
     }
     fn fallible_walk_domain_func_app(
         &mut self,
-        statement: &DomainFuncApp,
+        expr: &DomainFuncApp,
     ) -> Result<(), Self::Error> {
         let DomainFuncApp {
             domain_function,
             arguments,
             ..
-        } = statement;
+        } = expr;
         for arg in arguments {
             self.fallible_walk(arg)?;
         }
@@ -1327,48 +1327,48 @@ pub trait FallibleExprWalker: Sized {
         }
     }
     */
-    fn fallible_walk_inhale_exhale(&mut self, statement: &InhaleExhale) -> Result<(), Self::Error> {
+    fn fallible_walk_inhale_exhale(&mut self, expr: &InhaleExhale) -> Result<(), Self::Error> {
         let InhaleExhale {
             inhale_expr,
             exhale_expr,
             ..
-        } = statement;
+        } = expr;
         self.fallible_walk(inhale_expr)?;
         self.fallible_walk(exhale_expr)?;
         Ok(())
     }
 
-    fn fallible_walk_downcast(&mut self, statement: &DowncastExpr) -> Result<(), Self::Error> {
+    fn fallible_walk_downcast(&mut self, expr: &DowncastExpr) -> Result<(), Self::Error> {
         let DowncastExpr {
             base, enum_place, ..
-        } = statement;
+        } = expr;
         self.fallible_walk(base)?;
         self.fallible_walk(enum_place)?;
         Ok(())
     }
 
-    fn fallible_walk_snap_app(&mut self, statement: &SnapApp) -> Result<(), Self::Error> {
-        let SnapApp { base, .. } = statement;
+    fn fallible_walk_snap_app(&mut self, expr: &SnapApp) -> Result<(), Self::Error> {
+        let SnapApp { base, .. } = expr;
         self.fallible_walk(base)
     }
 
-    fn fallible_walk_container_op(&mut self, statement: &ContainerOp) -> Result<(), Self::Error> {
-        let ContainerOp { left, right, .. } = statement;
+    fn fallible_walk_container_op(&mut self, expr: &ContainerOp) -> Result<(), Self::Error> {
+        let ContainerOp { left, right, .. } = expr;
         self.fallible_walk(left)?;
         self.fallible_walk(right)?;
         Ok(())
     }
 
-    fn fallible_walk_seq(&mut self, statement: &Seq) -> Result<(), Self::Error> {
-        let Seq { typ, elements, .. } = statement;
+    fn fallible_walk_seq(&mut self, expr: &Seq) -> Result<(), Self::Error> {
+        let Seq { typ, elements, .. } = expr;
         for elem in elements {
             self.fallible_walk(elem)?;
         }
         self.fallible_walk_type(typ)
     }
 
-    fn fallible_walk_cast(&mut self, statement: &Cast) -> Result<(), Self::Error> {
-        let Cast { base, .. } = statement;
+    fn fallible_walk_cast(&mut self, expr: &Cast) -> Result<(), Self::Error> {
+        let Cast { base, .. } = expr;
         self.fallible_walk(base)
     }
 }

From ddc7e8209ef5ea482c90ef2cdcd64b248befe4e0 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 20:41:22 +0100
Subject: [PATCH 09/19] Make warning function more general

---
 prusti-interface/src/prusti_error.rs          | 4 ++--
 prusti-viper/src/encoder/procedure_encoder.rs | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs
index c0515c24e13..dfe78656361 100644
--- a/prusti-interface/src/prusti_error.rs
+++ b/prusti-interface/src/prusti_error.rs
@@ -101,10 +101,10 @@ impl PrustiError {
     }
 
     /// Issue with loop invariants (e.g. cannot automatically include loop guard)
-    pub fn loop_invariant<S: ToString>(message: S, span: MultiSpan) -> Self {
+    pub fn warning<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
         let mut err = PrustiError::new(
-            format!("[Prusti: loop invariant] {}", message.to_string()),
+            format!("[Prusti: warning] {}", message.to_string()),
             span
         );
         err.is_error = false;
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 475deb31846..c26fa668a07 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -832,7 +832,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             // Multispan to highlight both
             let span = MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().flatten().collect());
             // It's only a warning so we might as well emit it straight away
-            PrustiError::loop_invariant(warning_msg, span).emit(self.encoder.env());
+            PrustiError::warning(warning_msg, span).emit(self.encoder.env());
             None
         };
 

From ef272f05d3cba83eb8f69a4ea59d048514a8dfa6 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 28 Feb 2022 21:07:07 +0100
Subject: [PATCH 10/19] Fmt fix

---
 vir/defs/polymorphic/ast/expr_transformers.rs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/vir/defs/polymorphic/ast/expr_transformers.rs b/vir/defs/polymorphic/ast/expr_transformers.rs
index 107eabda8b1..f2d59447af9 100644
--- a/vir/defs/polymorphic/ast/expr_transformers.rs
+++ b/vir/defs/polymorphic/ast/expr_transformers.rs
@@ -1293,10 +1293,7 @@ pub trait FallibleExprWalker: Sized {
         }
         self.fallible_walk_type(return_type)
     }
-    fn fallible_walk_domain_func_app(
-        &mut self,
-        expr: &DomainFuncApp,
-    ) -> Result<(), Self::Error> {
+    fn fallible_walk_domain_func_app(&mut self, expr: &DomainFuncApp) -> Result<(), Self::Error> {
         let DomainFuncApp {
             domain_function,
             arguments,

From 2b0306dcf1eeb1b89df3c20fa20d8ca70470ae79 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Tue, 1 Mar 2022 09:59:37 +0100
Subject: [PATCH 11/19] Fix comment

---
 prusti-interface/src/prusti_error.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs
index dfe78656361..24c97bdf009 100644
--- a/prusti-interface/src/prusti_error.rs
+++ b/prusti-interface/src/prusti_error.rs
@@ -100,7 +100,7 @@ impl PrustiError {
         )
     }
 
-    /// Issue with loop invariants (e.g. cannot automatically include loop guard)
+    /// Report a non-fatal issue (e.g. cannot automatically include loop guard as an invariant)
     pub fn warning<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
         let mut err = PrustiError::new(

From e1f3e66b198705c4c849c30fd2fa7b055bbe25e0 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Wed, 23 Mar 2022 16:04:59 +0100
Subject: [PATCH 12/19] Change asserts to assumes after unrolling

Compared to not unrolling if we run into an assert
---
 prusti-viper/src/encoder/procedure_encoder.rs | 39 +++++++++++++++----
 1 file changed, 32 insertions(+), 7 deletions(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index db9882b43b7..57b2caad28f 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -529,10 +529,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 let expr = self.fold(statement.expr.clone());
                 self.preconds.push(expr);
             }
-            fn walk_assert(&mut self, statement: &vir::Assert) {
-                let expr = self.fold(statement.expr.clone());
-                self.preconds.push(expr);
-            }
             fn walk_expr(&mut self, expr: &vir::Expr) {
                 self.fold(expr.clone());
             }
@@ -593,18 +589,41 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let bb = &self.cfg_method.basic_blocks[block.block_index];
         let mut preconds: Vec<_> = bb.stmts.iter().flat_map(|stmt| self.stmt_preconditions(stmt)).collect();
         match &bb.successor {
-            Successor::Undefined => {}
-            Successor::Return => {}
+            Successor::Undefined => (),
+            Successor::Return => (),
             Successor::Goto(cbi) => preconds.extend(self.block_preconditions(cbi)),
             Successor::GotoSwitch(succs, def) => {
                 preconds.extend(
                     succs.iter().flat_map(|cond_bb| self.block_preconditions(&cond_bb.1))
                 );
                 preconds.extend(self.block_preconditions(def));
-            },
+            }
         }
         preconds
     }
+    fn block_assert_to_assume(&mut self, block: &CfgBlockIndex) {
+        let bb = &mut self.cfg_method.basic_blocks[block.block_index];
+        for stmt in &mut bb.stmts {
+            match stmt {
+                vir::Stmt::Assert(assert) => {
+                    let expr = assert.expr.clone();
+                    *stmt = vir::Stmt::Inhale(vir::Inhale { expr });
+                }
+                _ => (),
+            }
+        }
+        match bb.successor.clone() {
+            Successor::Undefined => (),
+            Successor::Return => (),
+            Successor::Goto(cbi) => self.block_assert_to_assume(&cbi),
+            Successor::GotoSwitch(succs, def) => {
+                for (_, succ) in succs {
+                    self.block_assert_to_assume(&succ);
+                }
+                self.block_assert_to_assume(&def)
+            }
+        }
+    }
 
     /// Encodes a loop.
     ///
@@ -803,6 +822,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 loop_depth,
                 return_block,
             )?;
+            if let Some(mid_g_head) = &mid_g.0 {
+                self.block_assert_to_assume(mid_g_head);
+            }
 
             // Encode the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end)
             let mid_b1 = self.encode_blocks_group(
@@ -811,6 +833,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 loop_depth,
                 return_block,
             )?;
+            if let Some(mid_b1_head) = &mid_b1.0 {
+                self.block_assert_to_assume(mid_b1_head);
+            }
             // Save for later linking up
             Some((mid_g, mid_b1))
         } else {

From 6a3b715a83434f1c3dfe6b7813c0685f83db6757 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Fri, 22 Apr 2022 17:43:33 +0200
Subject: [PATCH 13/19] Clippy fix

---
 prusti-viper/src/encoder/procedure_encoder.rs | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 3309c196022..fa605780aba 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -607,12 +607,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     fn block_assert_to_assume(&mut self, block: &CfgBlockIndex) {
         let bb = &mut self.cfg_method.basic_blocks[block.block_index];
         for stmt in &mut bb.stmts {
-            match stmt {
-                vir::Stmt::Assert(assert) => {
-                    let expr = assert.expr.clone();
-                    *stmt = vir::Stmt::Inhale(vir::Inhale { expr });
-                }
-                _ => (),
+            if let vir::Stmt::Assert(assert) = stmt {
+                let expr = assert.expr.clone();
+                *stmt = vir::Stmt::Inhale(vir::Inhale { expr });
             }
         }
         match bb.successor.clone() {

From df53a1e53fb57a765ee1c0737ed9c33144432af1 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Fri, 22 Apr 2022 18:37:04 +0200
Subject: [PATCH 14/19] Track pure functions preventing unrolling

And report them in the warning
---
 prusti-viper/src/encoder/procedure_encoder.rs | 37 +++++++++++++------
 1 file changed, 25 insertions(+), 12 deletions(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index fa605780aba..b66220f9caa 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -512,11 +512,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         Ok(still_unresolved_edges)
     }
 
-    fn stmt_preconditions(&self, stmt: &vir::Stmt) -> Vec<vir::Expr> {
+    fn stmt_preconditions(&self, stmt: &vir::Stmt) -> Vec<(Option<String>, vir::Expr)> {
         use vir::{ExprFolder, StmtWalker};
         struct FindFnApps<'a, 'b, 'c> {
             recurse: bool,
-            preconds: Vec<vir::Expr>,
+            preconds: Vec<(Option<String>, vir::Expr)>,
             encoder: &'a Encoder<'b, 'c>,
         }
         fn is_const_true(expr: &vir::Expr) -> bool {
@@ -527,10 +527,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 })
             )
         }
+        impl<'a, 'b, 'c> FindFnApps<'a, 'b, 'c> {
+            fn push_precond(&mut self, expr: vir::Expr, fn_name: Option<String>) {
+                let expr = self.fold(expr);
+                if !is_const_true(&expr) {
+                    self.preconds.push((fn_name, expr));
+                }
+            }
+        }
         impl<'a, 'b, 'c> StmtWalker for FindFnApps<'a, 'b, 'c> {
             fn walk_exhale(&mut self, statement: &vir::Exhale) {
-                let expr = self.fold(statement.expr.clone());
-                self.preconds.push(expr);
+                self.push_precond(statement.expr.clone(), None);
             }
             fn walk_expr(&mut self, expr: &vir::Expr) {
                 self.fold(expr.clone());
@@ -545,9 +552,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     let pres = self.encoder.get_function(&identifier).unwrap().pres.clone();
                     // Avoid recursively collecting preconditions: they should be self-framing anyway
                     self.recurse = false;
-                    let pres = pres.into_iter().map(|expr| self.fold(expr)).collect::<Vec<_>>();
+                    let pres: vir::Expr = pres.into_iter().fold(true.into(), |acc, expr| vir_expr! { [acc] && [expr] });
+                    self.push_precond(pres, Some(function_name));
                     self.recurse = true;
-                    self.preconds.extend(pres);
 
                     for arg in arguments {
                         self.fold(arg);
@@ -586,9 +593,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             recurse: true, preconds: Vec::new(), encoder: self.encoder
         };
         walker.walk(stmt);
-        walker.preconds.into_iter().filter(|exp| !is_const_true(exp)).collect()
+        walker.preconds
     }
-    fn block_preconditions(&self, block: &CfgBlockIndex) -> Vec<vir::Expr> {
+    fn block_preconditions(&self, block: &CfgBlockIndex) -> Vec<(Option<String>, vir::Expr)> {
         let bb = &self.cfg_method.basic_blocks[block.block_index];
         let mut preconds: Vec<_> = bb.stmts.iter().flat_map(|stmt| self.stmt_preconditions(stmt)).collect();
         match &bb.successor {
@@ -840,10 +847,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             Some((mid_g, mid_b1))
         } else {
             // Cannot add loop guard to loop invariant
-            let warning_msg = "the loop guard was not automatically added as a `body_invariant` \
-                (it requires the viper preconditions: [".to_string() + &preconds.iter().map(|pe|
-                    format!("{}", pe)
-                ).collect::<Vec<_>>().join(", ") + "] to hold)";
+            let fn_names: Vec<_> = preconds.iter().filter_map(|(name, _)| name.as_ref()).map(|name| {
+                assert!(name.starts_with("m_"));
+                &name[2..]
+            }).collect();
+            let warning_msg = if fn_names.len() == 0 {
+                "the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()
+            } else {
+                "the loop guard was not automatically added as a `body_invariant!(...)`, \
+                due to the following pure functions with preconditions: [".to_string() + &fn_names.join(", ") + "]"
+            };
             // Span of loop guard
             let span_lg = loop_guard_evaluation.last().map(|bb| self.mir_encoder.get_span_of_basic_block(*bb));
             // Span of entire loop body before inv; the last elem (if any) will be the `body_invariant!(...)` bb

From 51f731215f309ac6b1734f2e9a094a00542953bb Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Fri, 22 Apr 2022 18:46:30 +0200
Subject: [PATCH 15/19] Clippy fix

---
 prusti-viper/src/encoder/procedure_encoder.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index b66220f9caa..cc6787c9261 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -851,7 +851,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 assert!(name.starts_with("m_"));
                 &name[2..]
             }).collect();
-            let warning_msg = if fn_names.len() == 0 {
+            let warning_msg = if fn_names.is_empty() {
                 "the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()
             } else {
                 "the loop guard was not automatically added as a `body_invariant!(...)`, \

From 4ada2cda6a8d935219abd7a4e578554f267cda2c Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Wed, 27 Apr 2022 11:26:59 +0200
Subject: [PATCH 16/19] Only emit warning on verification failure

---
 prusti-interface/src/environment/mod.rs       | 10 ++++++++--
 prusti-interface/src/prusti_error.rs          |  4 +++-
 prusti-viper/src/encoder/procedure_encoder.rs |  3 +--
 3 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs
index c66a35ee65f..3b5e98b02c1 100644
--- a/prusti-interface/src/environment/mod.rs
+++ b/prusti-interface/src/environment/mod.rs
@@ -75,6 +75,7 @@ pub struct Environment<'tcx> {
     bodies: RefCell<HashMap<LocalDefId, CachedBody<'tcx>>>,
     external_bodies: RefCell<HashMap<DefId, CachedExternalBody<'tcx>>>,
     tcx: TyCtxt<'tcx>,
+    warn_buffer: RefCell<Vec<rustc_errors::Diagnostic>>,
 }
 
 impl<'tcx> Environment<'tcx> {
@@ -84,6 +85,7 @@ impl<'tcx> Environment<'tcx> {
             tcx,
             bodies: RefCell::new(HashMap::new()),
             external_bodies: RefCell::new(HashMap::new()),
+            warn_buffer: RefCell::new(Vec::new()),
         }
     }
 
@@ -161,10 +163,13 @@ impl<'tcx> Environment<'tcx> {
                 diagnostic.note(note_msg);
             }
         }
+        for warn in self.warn_buffer.borrow().iter() {
+            self.tcx.sess.diagnostic().emit_diagnostic(warn);
+        }
         diagnostic.emit();
     }
 
-    /// Emits an error message.
+    /// Buffers a warning message, to be emitted on error.
     pub fn span_warn_with_help_and_notes<S: Into<MultiSpan> + Clone>(
         &self,
         sp: S,
@@ -184,7 +189,8 @@ impl<'tcx> Environment<'tcx> {
                 diagnostic.note(note_msg);
             }
         }
-        diagnostic.emit();
+        // Possible to use `diagnostic.emit()` here to avoid buffering
+        diagnostic.buffer(&mut self.warn_buffer.borrow_mut());
     }
 
     /// Returns true if an error has been emitted
diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs
index a3f3459c961..bf037613d5f 100644
--- a/prusti-interface/src/prusti_error.rs
+++ b/prusti-interface/src/prusti_error.rs
@@ -162,7 +162,9 @@ impl PrustiError {
         self.notes.push((message.to_string(), opt_span));
     }
 
-    /// Report the encoding error using the compiler's interface
+    /// Report the encoding error using the compiler's interface.
+    /// Warnings are not immediately emitted, but buffered and only shown
+    /// if an error is emitted (i.e. verification failure)
     pub fn emit(self, env: &Environment) {
         assert!(!self.is_disabled);
         if self.is_error {
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 772d04a03d5..f63a2f5c1c1 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -848,8 +848,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         } else {
             // Cannot add loop guard to loop invariant
             let fn_names: Vec<_> = preconds.iter().filter_map(|(name, _)| name.as_ref()).map(|name| {
-                assert!(name.starts_with("m_"));
-                &name[2..]
+                if name.starts_with("m_") { &name[2..] } else { &name[..] }
             }).collect();
             let warning_msg = if fn_names.is_empty() {
                 "the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()

From 4ed6b781a26b980d4b71fd50dc7bd1b9fca36a2a Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Fri, 13 May 2022 16:43:46 +0200
Subject: [PATCH 17/19] Distinguish between warning types

---
 prusti-interface/src/environment/mod.rs | 53 +++++++++++++++----------
 prusti-interface/src/prusti_error.rs    | 50 +++++++++++++++++------
 2 files changed, 69 insertions(+), 34 deletions(-)

diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs
index 00f16b47efa..7cfbc41eebe 100644
--- a/prusti-interface/src/environment/mod.rs
+++ b/prusti-interface/src/environment/mod.rs
@@ -16,7 +16,7 @@ use rustc_middle::ty::subst::{Subst, SubstsRef};
 use rustc_trait_selection::infer::{InferCtxtExt, TyCtxtInferExt};
 use std::path::PathBuf;
 
-use rustc_errors::MultiSpan;
+use rustc_errors::{DiagnosticBuilder, EmissionGuarantee, MultiSpan};
 use rustc_span::{Span, symbol::Symbol};
 use std::collections::HashSet;
 use log::{debug, trace};
@@ -144,15 +144,12 @@ impl<'tcx> Environment<'tcx> {
     //     self.state.session.span_err(sp, msg);
     // }
 
-    /// Emits an error message.
-    pub fn span_err_with_help_and_notes<S: Into<MultiSpan> + Clone>(
-        &self,
+    fn configure_diagnostic<S: Into<MultiSpan> + Clone, T: EmissionGuarantee>(
+        diagnostic: &mut DiagnosticBuilder<T>,
         sp: S,
-        msg: &str,
         help: &Option<String>,
-        notes: &[(String, Option<S>)],
+        notes: &[(String, Option<S>)]
     ) {
-        let mut diagnostic = self.tcx.sess.struct_err(msg);
         diagnostic.set_span(sp);
         if let Some(help_msg) = help {
             diagnostic.help(help_msg);
@@ -164,13 +161,25 @@ impl<'tcx> Environment<'tcx> {
                 diagnostic.note(note_msg);
             }
         }
-        for warn in self.warn_buffer.borrow().iter() {
+    }
+
+    /// Emits an error message.
+    pub fn span_err_with_help_and_notes<S: Into<MultiSpan> + Clone>(
+        &self,
+        sp: S,
+        msg: &str,
+        help: &Option<String>,
+        notes: &[(String, Option<S>)],
+    ) {
+        let mut diagnostic = self.tcx.sess.struct_err(msg);
+        Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
+        for warn in self.warn_buffer.borrow_mut().iter_mut() {
             self.tcx.sess.diagnostic().emit_diagnostic(warn);
         }
         diagnostic.emit();
     }
 
-    /// Buffers a warning message, to be emitted on error.
+    /// Emits a warning message.
     pub fn span_warn_with_help_and_notes<S: Into<MultiSpan> + Clone>(
         &self,
         sp: S,
@@ -179,18 +188,20 @@ impl<'tcx> Environment<'tcx> {
         notes: &[(String, Option<S>)],
     ) {
         let mut diagnostic = self.tcx.sess.struct_warn(msg);
-        diagnostic.set_span(sp);
-        if let Some(help_msg) = help {
-            diagnostic.help(help_msg);
-        }
-        for (note_msg, opt_note_sp) in notes {
-            if let Some(note_sp) = opt_note_sp {
-                diagnostic.span_note(note_sp.clone(), note_msg);
-            } else {
-                diagnostic.note(note_msg);
-            }
-        }
-        // Possible to use `diagnostic.emit()` here to avoid buffering
+        Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
+        diagnostic.emit();
+    }
+
+    /// Buffers a warning message, to be emitted on error.
+    pub fn span_warn_on_err_with_help_and_notes<S: Into<MultiSpan> + Clone>(
+        &self,
+        sp: S,
+        msg: &str,
+        help: &Option<String>,
+        notes: &[(String, Option<S>)],
+    ) {
+        let mut diagnostic = self.tcx.sess.struct_warn(msg);
+        Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
         diagnostic.buffer(&mut self.warn_buffer.borrow_mut());
     }
 
diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs
index 90c9bc674c5..6367f04193b 100644
--- a/prusti-interface/src/prusti_error.rs
+++ b/prusti-interface/src/prusti_error.rs
@@ -21,7 +21,7 @@ use ::log::warn;
 /// `SpannedEncodingError` and similar types to something less confusing.)
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct PrustiError {
-    is_error: bool,
+    kind: PrustiErrorKind,
     /// If `true`, it should not be reported to the user. We need this in cases
     /// when the same error could be reported twice.
     ///
@@ -34,6 +34,13 @@ pub struct PrustiError {
     help: Option<String>,
     notes: Vec<(String, Option<MultiSpan>)>,
 }
+/// Determines how a `PrustiError` is reported.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum PrustiErrorKind {
+    Error, Warning,
+    /// A warning which is only shown if at least one error is emitted.
+    WarningOnError,
+}
 
 impl PartialOrd for PrustiError {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
@@ -51,7 +58,7 @@ impl PrustiError {
     /// Private constructor. Use one of the following methods.
     fn new(message: String, span: MultiSpan) -> Self {
         PrustiError {
-            is_error: true,
+            kind: PrustiErrorKind::Error,
             is_disabled: false,
             message,
             span,
@@ -101,14 +108,26 @@ impl PrustiError {
         )
     }
 
-    /// Report a non-fatal issue (e.g. cannot automatically include loop guard as an invariant)
+    /// Report a non-fatal issue
     pub fn warning<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
         let mut err = PrustiError::new(
             format!("[Prusti: warning] {}", message.to_string()),
             span
         );
-        err.is_error = false;
+        err.kind = PrustiErrorKind::Warning;
+        err
+    }
+
+    /// Report a non-fatal issue only if there are errors
+    /// (e.g. cannot automatically include loop guard as an invariant)
+    pub fn warning_on_error<S: ToString>(message: S, span: MultiSpan) -> Self {
+        check_message(message.to_string());
+        let mut err = PrustiError::new(
+            format!("[Prusti: warning] {}", message.to_string()),
+            span
+        );
+        err.kind = PrustiErrorKind::WarningOnError;
         err
     }
 
@@ -133,11 +152,11 @@ impl PrustiError {
 
     /// Set that this Prusti error should be reported as a warning to the user
     pub fn set_warning(&mut self) {
-        self.is_error = false;
+        self.kind = PrustiErrorKind::Warning;
     }
 
     pub fn is_error(&self) -> bool {
-        self.is_error
+        matches!(self.kind, PrustiErrorKind::Error)
     }
 
     // FIXME: This flag is a temporary workaround for having duplicate errors
@@ -168,21 +187,26 @@ impl PrustiError {
     /// if an error is emitted (i.e. verification failure)
     pub fn emit(self, env: &Environment) {
         assert!(!self.is_disabled);
-        if self.is_error {
-            env.span_err_with_help_and_notes(
+        match self.kind {
+            PrustiErrorKind::Error => env.span_err_with_help_and_notes(
                 self.span,
                 &self.message,
                 &self.help,
                 &self.notes,
-            );
-        } else {
-            env.span_warn_with_help_and_notes(
+            ),
+            PrustiErrorKind::Warning => env.span_warn_with_help_and_notes(
                 self.span,
                 &self.message,
                 &self.help,
                 &self.notes,
-            );
-        }
+            ),
+            PrustiErrorKind::WarningOnError => env.span_warn_on_err_with_help_and_notes(
+                self.span,
+                &self.message,
+                &self.help,
+                &self.notes,
+            ),
+        };
     }
 
     /// Cancel the error.

From 0eddf8a9c23bee0a1f0e940942733fe8f73fb837 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Fri, 13 May 2022 16:44:02 +0200
Subject: [PATCH 18/19] clippy fix

---
 prusti-viper/src/encoder/procedure_encoder.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 6862de3a2e7..230f8e299e0 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -856,7 +856,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         } else {
             // Cannot add loop guard to loop invariant
             let fn_names: Vec<_> = preconds.iter().filter_map(|(name, _)| name.as_ref()).map(|name| {
-                if name.starts_with("m_") { &name[2..] } else { &name[..] }
+                name.strip_prefix("m_").unwrap_or(name)
             }).collect();
             let warning_msg = if fn_names.is_empty() {
                 "the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()

From caee09bfe3947fdc8a41adc3ccf04e66afd39bf7 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Sat, 21 May 2022 17:01:27 +0200
Subject: [PATCH 19/19] Update test with new expected errors

---
 .../fail/optimizations/purification/test1.rs       | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs b/prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs
index 6ffbc8f1879..bd358569c12 100644
--- a/prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs
+++ b/prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs
@@ -5,20 +5,20 @@ use prusti_contracts::*;
 fn test1() {
     let mut i = 0;
     while i < 5 {
-        i += 1;     //~ ERROR: attempt to add with overflow
+        i += 1;
     }
     let mut j = 0;
-    assert!(i == j);
+    assert!(i == j);     //~ ERROR: the asserted expression might not hold
 }
 
 fn test2() {
     let mut i = 0;
     while i < 5 {
-        assert!(i < 5);  //~ ERROR: the asserted expression might not hold
+        assert!(i < 5);
         i += 1;
     }
     let mut j = 0;
-    assert!(i == j);
+    assert!(i == j);     //~ ERROR: the asserted expression might not hold
 }
 
 fn test3() {
@@ -35,7 +35,7 @@ fn test4(v: &mut[i32]) {
     let mut zero_num_start = 0;
     let mut i = 0;
     while i < v.len() {
-        assert!(i < v.len()); //~ ERROR: the asserted expression might not hold
+        assert!(i < v.len());
         i += 1;
     }
 }
@@ -44,8 +44,8 @@ fn test5(v: &mut[i32]) {
     let mut zero_num_start = 0;
     let mut i = 0;
     while i < v.len() {
-        if v[i] == 0 {  //~ ERROR: the array or slice index may be out of bounds
-            zero_num_start += 1;
+        if v[i] == 0 {
+            zero_num_start += 1; //~ ERROR: attempt to add with overflow
         }
         i += 1;
     }